[smt_convt] Fix usage of `use_array_of_bool` #6004

SaswatPadhi · 2021-04-03T01:10:31Z

Several SMT translation routines were not respecting use_array_of_bool, or led to a buggy SMT translation when they used it.

This change ensures consistent usage of this option across all array-related translation routines.

Each commit message has a non-empty body, explaining why the change was made.
NA ~~Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.~~
NA ~~The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/~~
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
NA ~~My commit message includes data points confirming performance improvements (if claimed).~~
My PR is restricted to a single feature or bugfix.
NA ~~White-space or formatting changes outside the feature-related changed lines are in commits of their own.~~

codecov · 2021-04-03T03:05:44Z

Codecov Report

Merging #6004 (28504a7) into develop (1c32785) will increase coverage by 0.13%.
The diff coverage is 84.00%.

❗ Current head 28504a7 differs from pull request most recent head 3e27734. Consider uploading reports for the commit 3e27734 to get more accurate results

@@             Coverage Diff             @@
##           develop    #6004      +/-   ##
===========================================
+ Coverage    74.11%   74.24%   +0.13%     
===========================================
  Files         1444     1444              
  Lines       157389   157415      +26     
===========================================
+ Hits        116646   116871     +225     
+ Misses       40743    40544     -199

Impacted Files	Coverage Δ
src/solvers/smt2/smt2_conv.cpp	`60.36% <63.63%> (+0.29%)`	⬆️
src/goto-instrument/loop_utils.cpp	`94.54% <100.00%> (+1.52%)`	⬆️
src/ansi-c/expr2c.cpp	`58.14% <0.00%> (+0.19%)`	⬆️
src/linking/linking.cpp	`49.69% <0.00%> (+0.30%)`	⬆️
src/solvers/flattening/boolbv_typecast.cpp	`49.82% <0.00%> (+0.34%)`	⬆️
src/ansi-c/c_typecheck_expr.cpp	`60.19% <0.00%> (+0.39%)`	⬆️
src/ansi-c/scanner.l	`41.67% <0.00%> (+0.52%)`	⬆️
src/util/simplify_expr_floatbv.cpp	`94.57% <0.00%> (+0.77%)`	⬆️
src/ansi-c/c_typecheck_code.cpp	`70.63% <0.00%> (+1.21%)`	⬆️
... and 6 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update a8cfa6f...3e27734. Read the comment docs.

tautschnig

Seems reasonable to me, but would you have any tests that newly pass with this fix?

SaswatPadhi · 2021-04-04T20:12:22Z

Thanks for taking a look, Michael.

The options --z3 and --cprover-smt2 set use_array_of_bool to true and so these fixes won't apply -- all of these fixes apply to cases when bool is modeled as (_ BitVec 1).

I wanted to include the test case from #6005, basically use --smt2 --z3 to run z3 with use_array_of_bool set to false, but unfortunately that won't pass because of other issues (use of quantifiers within QF logic: see #6005 for more details).

martin-cs

+1 to what @tautschnig says, test please!

SaswatPadhi · 2021-04-07T22:39:43Z

Thanks for the review, @martin-cs.

I am not sure how I could add a test for these changes ...
With --smt2 CBMC would perform the SMT encoding with use_array_of_bool = false but the result won't run with Z3 because it would also set the logic to QF_AUFBV.

Any ideas? cc: @tautschnig @kroening.

Some background on why I made this PR and how I tested it:

with --z3 CBMC produces (with use_array_of_bool = true) an SMT file that takes forever on Z3 -- no syntax error, but just really really slow
with --smt2 --z3 I was getting incorrect translations because use_array_of_bool was not handled correctly. With the changes proposed in this PR, the translation is correct and if I change the logic to ALL then Z3 reports unsat in a couple of seconds.

So there is some performance issue in Z3 that is triggered by --z3 encoding but not --smt2 encoding. But that should be in a separate PR. This just fixes translation errors with --smt2 encoding.

SaswatPadhi · 2021-04-15T03:24:16Z

After an offline discussion with @tautschnig, I have added a regression test to check the raw SMT2 output instead of running end-to-end against an SMT solver. Please take a look and see if it looks okay.

regression/cbmc/array_of_bool_as_bitvec/main.c

tautschnig · 2021-04-15T14:48:45Z

regression/cbmc/array_of_bool_as_bitvec/main.c

+  bool y[8];
+  bool *z = malloc(8 * sizeof(bool));
+
+  memset(y, 0, sizeof(y));
+  memset(z, 0, sizeof(8 * sizeof(bool)));


Wouldn't

bool y[8] = { 0 }; bool *z = calloc(8, sizeof(boo));

also do the trick, or does this not trigger the desired code paths? Likewise, is it actually necessary to use bool, or could _Bool or int equally be used?

Only __CPROVER_bool seems to trigger the desired code paths.
I have these bool variables (which are actually encoded as int) just to make sure their encoding is unaffected by the proposed changes.

I am not sure what _Bool is -- I will try this out and also modify the array initializations as you suggested.

Looks like _Bool doesn't trigger the code path either.

I have now implemented the changes as suggested.

Several SMT translation routines were not respecting `use_array_of_bool` or led to a buggy SMT translation when they used it. This change ensures consistent usage of this option across all array-related translation routines.

SaswatPadhi requested review from allredj, kroening, martin-cs, peterschrammel, romainbrenguier and tautschnig as code owners April 3, 2021 01:10

SaswatPadhi mentioned this pull request Apr 3, 2021

CBMC silently ignores syntax errors from SMT solver #6005

Closed

tautschnig reviewed Apr 3, 2021

View reviewed changes

martin-cs approved these changes Apr 6, 2021

View reviewed changes

SaswatPadhi force-pushed the use_array_of_bool_fix branch 2 times, most recently from 600ee90 to f31a8c6 Compare April 15, 2021 03:23

SaswatPadhi self-assigned this Apr 15, 2021

SaswatPadhi added aws Bugs or features of importance to AWS CBMC users bugfix SMT Backend Interface labels Apr 15, 2021

tautschnig reviewed Apr 15, 2021

View reviewed changes

regression/cbmc/array_of_bool_as_bitvec/main.c Outdated Show resolved Hide resolved

tautschnig reviewed Apr 15, 2021

View reviewed changes

regression/cbmc/array_of_bool_as_bitvec/main.c Outdated Show resolved Hide resolved

SaswatPadhi force-pushed the use_array_of_bool_fix branch 2 times, most recently from d2428d8 to 03248be Compare April 15, 2021 14:14

tautschnig reviewed Apr 15, 2021

View reviewed changes

SaswatPadhi force-pushed the use_array_of_bool_fix branch 2 times, most recently from 28504a7 to 15e40f9 Compare April 15, 2021 15:16

[smt_convt] Fix usage of use_array_of_bool

3e27734

Several SMT translation routines were not respecting `use_array_of_bool` or led to a buggy SMT translation when they used it. This change ensures consistent usage of this option across all array-related translation routines.

SaswatPadhi force-pushed the use_array_of_bool_fix branch from 15e40f9 to 3e27734 Compare April 15, 2021 15:18

SaswatPadhi merged commit 5914d75 into diffblue:develop Apr 15, 2021

SaswatPadhi deleted the use_array_of_bool_fix branch April 15, 2021 19:56

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[smt_convt] Fix usage of `use_array_of_bool` #6004

[smt_convt] Fix usage of `use_array_of_bool` #6004

Uh oh!

SaswatPadhi commented Apr 3, 2021 •

edited

Loading

Uh oh!

codecov bot commented Apr 3, 2021 •

edited

Loading

Uh oh!

tautschnig left a comment

Uh oh!

SaswatPadhi commented Apr 4, 2021

Uh oh!

martin-cs left a comment

Uh oh!

SaswatPadhi commented Apr 7, 2021

Uh oh!

SaswatPadhi commented Apr 15, 2021

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tautschnig Apr 15, 2021

Uh oh!

SaswatPadhi Apr 15, 2021

Uh oh!

SaswatPadhi Apr 15, 2021

Uh oh!

Uh oh!

[smt_convt] Fix usage of use_array_of_bool #6004

[smt_convt] Fix usage of use_array_of_bool #6004

Uh oh!

Conversation

SaswatPadhi commented Apr 3, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov bot commented Apr 3, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

SaswatPadhi commented Apr 4, 2021

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

SaswatPadhi commented Apr 7, 2021

Uh oh!

SaswatPadhi commented Apr 15, 2021

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tautschnig Apr 15, 2021

Choose a reason for hiding this comment

Uh oh!

SaswatPadhi Apr 15, 2021

Choose a reason for hiding this comment

Uh oh!

SaswatPadhi Apr 15, 2021

Choose a reason for hiding this comment

Uh oh!

Uh oh!

[smt_convt] Fix usage of `use_array_of_bool` #6004

[smt_convt] Fix usage of `use_array_of_bool` #6004

SaswatPadhi commented Apr 3, 2021 •

edited

Loading

codecov bot commented Apr 3, 2021 •

edited

Loading